$\forall$$A$:Type, $d$:DS($A$), $a$:$A$. dsdeq($d$;$a$) $\in$ EqDecider(dstype($A$; $d$; $a$))